ds:x:Id fp Type, da:k:Knd fp Type, n:, v:ecl-trans-tuple{i:l}(ds;da), L:event-info(ds;da) List,
m:.
ecl-trans-halt2(ds;da;ecl-add-throw(v;n))(m,L)

n = m   & ecl-trans-halt2(ds;da;v)(0,L)  ecl-trans-halt2(ds;da;v)(m,L)
 n = m   & 0<m & ecl-trans-halt2(ds;da;v)(m,L) 

latex

Definitions

b, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-h(v), ecl-trans-type(A), ecl-trans-state-from(v;z;L), ecl-trans-init(v), ecl-trans-tuple{i:l}(ds;da), t  T, x:A. B(x), P  Q, Id, x. t(x), a:A fp B(a), Knd, , event-info(ds;da), ecl-trans-halt2(ds;da;A), ecl-trans-state(v;L), ecl-add-throw(A;m), AB, False, A, P & Q, Prop, P  Q, i<j, p  q, p  q, P  Q, P  Q, b, , i=j, Unit, {T}

Lemmas

eqtt to assert, eqff to assert, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, assert of bor, iff functionality wrt iff, iff transitivity, assert of band, and functionality wrt iff, assert of lt int, bor wf, band wf, lt int wf, not wf, assert wf, le wf, event-info wf, ecl-trans-tuple wf, nat wf, Knd wf, fpf wf, Id wf, ecl-trans-state wf, ecl-trans-type wf